COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	The usual application of  Hoare-style semantics is in the  context of
C00008 00003	interactive programming system--for construction of reliable progs
C00009 00004
C00010 ENDMK
C⊗;
The usual application of  Hoare-style semantics is in the  context of
verification of fully  specified programs.  A program with assertions
is analyzed  and  verification conditions  are  generated.   Given  a
sufficient  set  of  assertions,  the  truth  of  these  verification
conditions will establish the correctness of the program.  

Objections  have been  raised concerning  the practically  of Hoare's
techniques: 

(1) the problem of discovering sufficient assertions is frequently as
difficult as writing the program; 

(2)  the  difficulties  of  generating  correct programs  are  better
handled by  "constructive" techniques  which  are applied  while  the
program  is being  written,  rather  than  attempting to  certify  an
existing program. 

The  first objection  stems from  at  least two  sources.   The usual
assertion language  is  a predicate-calculus  notation.    Frequently
programming constructs do not fit well into this language.  This is a
question which we plan to attack.  The more fundamental difficulty is
that it will always be  more difficult to give a  convincing argument
about correctness,  than just to  appeal to intuition.   Intuition is
frequently wrong;  that's when  we  have bugs.   Another  reason  for
difficulty stems from the rather poor state of programming practice. 
One  normally  thinks  of assertions  as  statements  about "what"  a
program does,  and thinks of  the program  as the  "how". The  "what"
might  be "permutes  the  elements" or  "see if  x  is a  conditional
expression";   the   programmer  usually   gives   the  "how"   as  a
representation  like  "t←x;x←y;y←t" or "(EQ (CAR  EXP) (QUOTE COND))".
Expressing the  "how" in  such representation-dependent  terms is  an
unnecessary source of difficult. 


The second  class of objections  stems from a  misunderstanding about
Hoare's  rules of inference.  There is no  reason why  these rules of
inference cannot be  used to guide the  construction of the  program.
Consider the "iteration rule":

              P{A}R, R∧S{B}R, R∧¬S⊃Q
              ______________________   
              P{A;R;while S do B}Q

This rule can be used in program construction as follows: "If we wish
to  use the iteration rule  to elaborate a variable  C in a partially
constructed program:

partially specified input assertion{ .....;C} partially specified output assertion

then we had better be prepared to justify the three subproblems above
the line." The  structure of the three subproblems can be used by the
programmer to continue his construction.  If some  of the subproblems
are  obviously   unattainable  then   the  user  might   withdraw  the
application of  the iteration rule.  The structure of the subproblems
might also help the user specify more of the  program or specify part
of the  assertion, R. The  point is that  there is a  stong interplay
between the construction of the  program and the construction of  the
assertions which are required by Hoare. 

This  interpretation  of  Hoare's  rules  is  surely  "constructive",
following  the  dictates  of  structured  programming;  and  if  the
programmer   uses   care   in   picking    representation-independent
programming  constructs  he  can   mitigate  the  complexity  of  the
construction-verification process. 

The preceding perspective on axiomatic semantics  leads us to believe
that a useful interactive programming system can and should be built.
This involves a command language to select rules, make substitutions,
prove lemmas, do simple  bookeeping, verify subprograms, or construct
program segments. 

interactive programming system--for construction of reliable progs
  get validation in at the level of construction
  based on style in book
  display-based

  abstract programming-specificstion lang
  selection of constructs
     examples -by structure

  manageability at informal &  possibilities at formal
    correctness question is addressed as program is being built

  transcripts as doc
    since it's by selection we can folllow trace of user commands

attempt to justify by experiment validity of struc
 students and practicioners

Further extensions
 from spec to pl
 constructs for multi-proc..